\begin{tabbing}
$\forall$\=${\it es}$:ES, $i$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$Prop),\+
\\[0ex]${\it init}$:\{$f$:$x$:Id fp$\rightarrow$ ${\it ds}$($x$)?Top$\mid$ $\forall$$x$:Id. $x$ $\in$ dom(${\it ds}$) $\Rightarrow$ $x$ $\in$ dom($f$) \}.
\-\\[0ex]$P$ holds in state ${\it init}$ $\Rightarrow$ $\exists$e@$i$ $\in$ Prop
\end{tabbing}